For purposes of analysis, it is often efficient and desirable to automate the reasoning about the complexity of software using tools and abstractions which can describe the properties and behavior of computer software. Computer software may often be formally described for the purposes of such analysis by specifying a set of constraints or axioms formalizing the relationships and operation of the software.
Automated theorem proving (ATP), or automated deduction, is currently a well-developed subfield of automated reasoning (AR). ATP is the proving of mathematical theorems by a computer program. Theorem provers are useful in a wide range of applications such as in computer software and hardware analysis, software systems requirements analysis, and compiler verification. One type of theorem prover is known as a satisfiability modulo theory or theorem (SMT) solver.
In many theorem solvers, including SMT solvers, it is important to consider the amount of time it takes a solver to solve theorems and the amount of computing resources (such as memory space or processor power) which may be required by the solver. Further, efficiency is an important goal in implementing these solvers, measured by, for example, the amount of time it takes a solver to prove a theorem.
SMT solvers have proven highly successful for program verification applications. Their ability to combine efficient quantifier reasoning with theory solvers for specialized domains, such as linear arithmetic or bit-vectors, makes SMT solvers particularly attractive.
Unfortunately, for quantifier instantiation, the wrong guidance may result in massively wasted search. To reduce the search space, a careful annotation of quantifiers using patterns can be used to guide quantifier instantiation to only involve terms matching the pattern annotations. Pattern annotations are either added by compilers that generate formulas, or by users, who annotate the patterns according to their best abilities, but sometimes with unintended results. Common mistakes are often repeated by several users when each user has to re-learn the same lessons from good and bad practices.